import java.util.*;
import java.io.*;

public class ROBDD {

	private static final class Func {
		private static final int TRUE = 0x7fffffff;
		private static final int FALSE = TRUE-1;

		private final int m_ciVar;
		private final Func m_cThen,m_cElse;

		Func(boolean b) {
			m_ciVar = b ? TRUE : FALSE;
			m_cThen = m_cElse = null;
		}

		Func(int iVar,Func t,Func e) {
			m_ciVar = iVar;
			m_cThen = t;
			m_cElse = e;
		}

		Func getThen(int iVar) {
			return iVar == m_ciVar ? m_cThen : this;
		}

		Func getElse(int iVar) {
			return iVar == m_ciVar ? m_cElse : this;
		}

		int getVar() {
			return m_ciVar;
		}

		boolean isTrue() {
			return m_ciVar == TRUE;
		}

		boolean isFalse() {
			return m_ciVar == FALSE;
		}

		boolean isConstant() {
			return isTrue() || isFalse();
		}

		void print(PrintStream p,Hashtable<Integer,String> varMap,HashSet<Func> printed,boolean bFirst) {
			if (printed.contains(this))
				return;
			printed.add(this);
			if (!bFirst)
				p.println(",");
			if (isConstant())
				p.println("l(\"" + this + "\",n(\"\",[a(\"OBJECT\",\"" + (isTrue() ? "1" : "0") + "\")],[]))");
			else {
				final String cName = varMap.get(m_ciVar);
				p.println("l(\"" + this + "\",n(\"\",[a(\"OBJECT\",\"" + cName + "\"),a(\"_GO\",\"ellipse\")],[");
				p.println("e(\"" + this + "->" + m_cThen + "\",[],r(\"" + m_cThen + "\"))");
				p.println(",");
				p.println("e(\"" + this + "->" + m_cElse + "\",[a(\"EDGEPATTERN\",\"dotted\")],r(\"" + m_cElse + "\"))");
				p.println("]))");
				m_cThen.print(p,varMap,printed,false);
				m_cElse.print(p,varMap,printed,false);
			}
		}
	}

	private static final class Triple {
		private final int m_ciVar;
		private final Func m_cThen;
		private final Func m_cElse;

		Triple(int iVar,Func fThen,Func fElse) {
			m_ciVar = iVar;
			m_cThen = fThen;
			m_cElse = fElse;
		}

		public boolean equals(Object obj) {
			if (obj instanceof Triple) {
				Triple arg = (Triple)obj;
				return arg.m_ciVar == m_ciVar && arg.m_cThen == m_cThen && arg.m_cElse == m_cElse;
			}
			return false;
		}

		public int hashCode() {
			return m_ciVar ^ m_cThen.hashCode() ^ m_cElse.hashCode();
		}
	}

	private final Func m_cTrue,m_cFalse;
	private int m_iNextVar;
	private Hashtable<String,Integer> m_VarMap;
	private Hashtable<Integer,String> m_RevVarMap;
	private Hashtable<Triple,Func> m_Unique;

	ROBDD() {
		m_cTrue = new Func(true);
		m_cFalse = new Func(false);
		m_iNextVar = 0;
		m_VarMap = new Hashtable<String,Integer>();
		m_RevVarMap = new Hashtable<Integer,String>();
		m_Unique = new Hashtable<Triple,Func>();
	}

	Func genTrue() {
		return m_cTrue;
	}

	Func genFalse() {
		return m_cFalse;
	}

	Func genVar(String name) {
		Integer var = m_VarMap.get(name);
		if (var == null) {
			var = m_iNextVar++;
			m_VarMap.put(name,var);
			m_RevVarMap.put(var,name);
		}
		Triple entry = new Triple(var,genTrue(),genFalse());
		Func res = m_Unique.get(entry);
		if (res == null) {
			res = new Func(var,genTrue(),genFalse());
			m_Unique.put(entry,res);
		}
		return res;
	}

	Func ite(Func i,Func t,Func e) {
		if (i.isTrue())
			return t;
		else if (i.isFalse())
			return e;
		else if (t.isTrue() && e.isFalse())
			return i;
		else {
			final int ciVar = Math.min(Math.min(i.getVar(),t.getVar()),e.getVar());
			final Func T = ite(i.getThen(ciVar),t.getThen(ciVar),e.getThen(ciVar));
			final Func E = ite(i.getElse(ciVar),t.getElse(ciVar),e.getElse(ciVar));
			if (T.equals(E))
				return T;
			final Triple entry = new Triple(ciVar,T,E);
			Func res = m_Unique.get(entry);
			if (res == null) {
				res = new Func(ciVar,T,E);
				m_Unique.put(entry,res);
			}
			return res;
		}
	}

	Func and(Func a,Func b) {
		return ite(a,b,genFalse());
	}

	Func or(Func a,Func b) {
		return ite(a,genTrue(),b);
	}

	Func not(Func a) {
		return ite(a,genFalse(),genTrue());
	}

	void print(PrintStream p,Func f) {
		p.println("[");
		f.print(p,m_RevVarMap,new HashSet<Func>(),true);
		p.println("]");
	}

	public static void main(String[] args) throws Exception {
		ROBDD bdd = new ROBDD();
		Func y = bdd.genVar("y");
		Func x = bdd.genVar("x");
		Func z = bdd.genVar("z");
		Func xOry = bdd.or(x,y);
		Func nzOrny = bdd.or(bdd.not(z),bdd.not(y));
		Func f = bdd.and(xOry,nzOrny);
		PrintStream p = new PrintStream(new FileOutputStream("/test.udg"));
//		bdd.print(p,x);
		bdd.print(p,f);
		p.close();
		//ProgStarter.startUDrawGraph(false,"test.udg");
	}
}
